↳ ITRS

  ↳ ITRStoIDPProof

z

eval(an, bn, cn, i, j) → Cond_eval2(&&(<@z(j, bn), <@z(i, an)), an, bn, cn, i, j)
eval(an, bn, cn, i, j) → Cond_eval1(&&(>=@z(j, bn), <@z(i, an)), an, bn, cn, i, j)
Cond_eval(TRUE, an, bn, cn, i, j) → eval(an, bn, +@z(cn, 1@z), +@z(i, 1@z), j)
eval(an, bn, cn, i, j) → Cond_eval(&&(<@z(j, bn), <@z(i, an)), an, bn, cn, i, j)
Cond_eval2(TRUE, an, bn, cn, i, j) → eval(an, bn, +@z(cn, 1@z), i, +@z(j, 1@z))
eval(an, bn, cn, i, j) → Cond_eval3(&&(<@z(j, bn), >=@z(i, an)), an, bn, cn, i, j)
Cond_eval3(TRUE, an, bn, cn, i, j) → eval(an, bn, +@z(cn, 1@z), i, +@z(j, 1@z))
Cond_eval1(TRUE, an, bn, cn, i, j) → eval(an, bn, +@z(cn, 1@z), +@z(i, 1@z), j)

eval(x0, x1, x2, x3, x4)
Cond_eval(TRUE, x0, x1, x2, x3, x4)
Cond_eval2(TRUE, x0, x1, x2, x3, x4)
Cond_eval3(TRUE, x0, x1, x2, x3, x4)
Cond_eval1(TRUE, x0, x1, x2, x3, x4)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

z

eval(an, bn, cn, i, j) → Cond_eval2(&&(<@z(j, bn), <@z(i, an)), an, bn, cn, i, j)
eval(an, bn, cn, i, j) → Cond_eval1(&&(>=@z(j, bn), <@z(i, an)), an, bn, cn, i, j)
Cond_eval(TRUE, an, bn, cn, i, j) → eval(an, bn, +@z(cn, 1@z), +@z(i, 1@z), j)
eval(an, bn, cn, i, j) → Cond_eval(&&(<@z(j, bn), <@z(i, an)), an, bn, cn, i, j)
Cond_eval2(TRUE, an, bn, cn, i, j) → eval(an, bn, +@z(cn, 1@z), i, +@z(j, 1@z))
eval(an, bn, cn, i, j) → Cond_eval3(&&(<@z(j, bn), >=@z(i, an)), an, bn, cn, i, j)
Cond_eval3(TRUE, an, bn, cn, i, j) → eval(an, bn, +@z(cn, 1@z), i, +@z(j, 1@z))
Cond_eval1(TRUE, an, bn, cn, i, j) → eval(an, bn, +@z(cn, 1@z), +@z(i, 1@z), j)

(0) -> (1), if ((+@z(i[0], 1@z) →^* i[1])∧(j[0] →^* j[1])∧(bn[0] →^* bn[1])∧(+@z(cn[0], 1@z) →^* cn[1])∧(an[0] →^* an[1]))

(0) -> (2), if ((+@z(i[0], 1@z) →^* i[2])∧(j[0] →^* j[2])∧(bn[0] →^* bn[2])∧(+@z(cn[0], 1@z) →^* cn[2])∧(an[0] →^* an[2]))

(0) -> (6), if ((+@z(i[0], 1@z) →^* i[6])∧(j[0] →^* j[6])∧(bn[0] →^* bn[6])∧(+@z(cn[0], 1@z) →^* cn[6])∧(an[0] →^* an[6]))

(0) -> (7), if ((+@z(i[0], 1@z) →^* i[7])∧(j[0] →^* j[7])∧(bn[0] →^* bn[7])∧(+@z(cn[0], 1@z) →^* cn[7])∧(an[0] →^* an[7]))

(1) -> (5), if ((cn[1] →^* cn[5])∧(i[1] →^* i[5])∧(an[1] →^* an[5])∧(bn[1] →^* bn[5])∧(j[1] →^* j[5])∧(&&(<@z(j[1], bn[1]), <@z(i[1], an[1])) →^* TRUE))

(2) -> (4), if ((cn[2] →^* cn[4])∧(i[2] →^* i[4])∧(an[2] →^* an[4])∧(bn[2] →^* bn[4])∧(j[2] →^* j[4])∧(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])) →^* TRUE))

(3) -> (1), if ((i[3] →^* i[1])∧(+@z(j[3], 1@z) →^* j[1])∧(bn[3] →^* bn[1])∧(+@z(cn[3], 1@z) →^* cn[1])∧(an[3] →^* an[1]))

(3) -> (2), if ((i[3] →^* i[2])∧(+@z(j[3], 1@z) →^* j[2])∧(bn[3] →^* bn[2])∧(+@z(cn[3], 1@z) →^* cn[2])∧(an[3] →^* an[2]))

(3) -> (6), if ((i[3] →^* i[6])∧(+@z(j[3], 1@z) →^* j[6])∧(bn[3] →^* bn[6])∧(+@z(cn[3], 1@z) →^* cn[6])∧(an[3] →^* an[6]))

(3) -> (7), if ((i[3] →^* i[7])∧(+@z(j[3], 1@z) →^* j[7])∧(bn[3] →^* bn[7])∧(+@z(cn[3], 1@z) →^* cn[7])∧(an[3] →^* an[7]))

(4) -> (1), if ((+@z(i[4], 1@z) →^* i[1])∧(j[4] →^* j[1])∧(bn[4] →^* bn[1])∧(+@z(cn[4], 1@z) →^* cn[1])∧(an[4] →^* an[1]))

(4) -> (2), if ((+@z(i[4], 1@z) →^* i[2])∧(j[4] →^* j[2])∧(bn[4] →^* bn[2])∧(+@z(cn[4], 1@z) →^* cn[2])∧(an[4] →^* an[2]))

(4) -> (6), if ((+@z(i[4], 1@z) →^* i[6])∧(j[4] →^* j[6])∧(bn[4] →^* bn[6])∧(+@z(cn[4], 1@z) →^* cn[6])∧(an[4] →^* an[6]))

(4) -> (7), if ((+@z(i[4], 1@z) →^* i[7])∧(j[4] →^* j[7])∧(bn[4] →^* bn[7])∧(+@z(cn[4], 1@z) →^* cn[7])∧(an[4] →^* an[7]))

(5) -> (1), if ((i[5] →^* i[1])∧(+@z(j[5], 1@z) →^* j[1])∧(bn[5] →^* bn[1])∧(+@z(cn[5], 1@z) →^* cn[1])∧(an[5] →^* an[1]))

(5) -> (2), if ((i[5] →^* i[2])∧(+@z(j[5], 1@z) →^* j[2])∧(bn[5] →^* bn[2])∧(+@z(cn[5], 1@z) →^* cn[2])∧(an[5] →^* an[2]))

(5) -> (6), if ((i[5] →^* i[6])∧(+@z(j[5], 1@z) →^* j[6])∧(bn[5] →^* bn[6])∧(+@z(cn[5], 1@z) →^* cn[6])∧(an[5] →^* an[6]))

(5) -> (7), if ((i[5] →^* i[7])∧(+@z(j[5], 1@z) →^* j[7])∧(bn[5] →^* bn[7])∧(+@z(cn[5], 1@z) →^* cn[7])∧(an[5] →^* an[7]))

(6) -> (0), if ((cn[6] →^* cn[0])∧(i[6] →^* i[0])∧(an[6] →^* an[0])∧(bn[6] →^* bn[0])∧(j[6] →^* j[0])∧(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])) →^* TRUE))

(7) -> (3), if ((cn[7] →^* cn[3])∧(i[7] →^* i[3])∧(an[7] →^* an[3])∧(bn[7] →^* bn[3])∧(j[7] →^* j[3])∧(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])) →^* TRUE))

eval(x0, x1, x2, x3, x4)
Cond_eval(TRUE, x0, x1, x2, x3, x4)
Cond_eval2(TRUE, x0, x1, x2, x3, x4)
Cond_eval3(TRUE, x0, x1, x2, x3, x4)
Cond_eval1(TRUE, x0, x1, x2, x3, x4)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

z

(0) -> (1), if ((+@z(i[0], 1@z) →^* i[1])∧(j[0] →^* j[1])∧(bn[0] →^* bn[1])∧(+@z(cn[0], 1@z) →^* cn[1])∧(an[0] →^* an[1]))

(0) -> (2), if ((+@z(i[0], 1@z) →^* i[2])∧(j[0] →^* j[2])∧(bn[0] →^* bn[2])∧(+@z(cn[0], 1@z) →^* cn[2])∧(an[0] →^* an[2]))

(0) -> (6), if ((+@z(i[0], 1@z) →^* i[6])∧(j[0] →^* j[6])∧(bn[0] →^* bn[6])∧(+@z(cn[0], 1@z) →^* cn[6])∧(an[0] →^* an[6]))

(0) -> (7), if ((+@z(i[0], 1@z) →^* i[7])∧(j[0] →^* j[7])∧(bn[0] →^* bn[7])∧(+@z(cn[0], 1@z) →^* cn[7])∧(an[0] →^* an[7]))

(1) -> (5), if ((cn[1] →^* cn[5])∧(i[1] →^* i[5])∧(an[1] →^* an[5])∧(bn[1] →^* bn[5])∧(j[1] →^* j[5])∧(&&(<@z(j[1], bn[1]), <@z(i[1], an[1])) →^* TRUE))

(2) -> (4), if ((cn[2] →^* cn[4])∧(i[2] →^* i[4])∧(an[2] →^* an[4])∧(bn[2] →^* bn[4])∧(j[2] →^* j[4])∧(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])) →^* TRUE))

(3) -> (1), if ((i[3] →^* i[1])∧(+@z(j[3], 1@z) →^* j[1])∧(bn[3] →^* bn[1])∧(+@z(cn[3], 1@z) →^* cn[1])∧(an[3] →^* an[1]))

(3) -> (2), if ((i[3] →^* i[2])∧(+@z(j[3], 1@z) →^* j[2])∧(bn[3] →^* bn[2])∧(+@z(cn[3], 1@z) →^* cn[2])∧(an[3] →^* an[2]))

(3) -> (6), if ((i[3] →^* i[6])∧(+@z(j[3], 1@z) →^* j[6])∧(bn[3] →^* bn[6])∧(+@z(cn[3], 1@z) →^* cn[6])∧(an[3] →^* an[6]))

(3) -> (7), if ((i[3] →^* i[7])∧(+@z(j[3], 1@z) →^* j[7])∧(bn[3] →^* bn[7])∧(+@z(cn[3], 1@z) →^* cn[7])∧(an[3] →^* an[7]))

(4) -> (1), if ((+@z(i[4], 1@z) →^* i[1])∧(j[4] →^* j[1])∧(bn[4] →^* bn[1])∧(+@z(cn[4], 1@z) →^* cn[1])∧(an[4] →^* an[1]))

(4) -> (2), if ((+@z(i[4], 1@z) →^* i[2])∧(j[4] →^* j[2])∧(bn[4] →^* bn[2])∧(+@z(cn[4], 1@z) →^* cn[2])∧(an[4] →^* an[2]))

(4) -> (6), if ((+@z(i[4], 1@z) →^* i[6])∧(j[4] →^* j[6])∧(bn[4] →^* bn[6])∧(+@z(cn[4], 1@z) →^* cn[6])∧(an[4] →^* an[6]))

(4) -> (7), if ((+@z(i[4], 1@z) →^* i[7])∧(j[4] →^* j[7])∧(bn[4] →^* bn[7])∧(+@z(cn[4], 1@z) →^* cn[7])∧(an[4] →^* an[7]))

(5) -> (1), if ((i[5] →^* i[1])∧(+@z(j[5], 1@z) →^* j[1])∧(bn[5] →^* bn[1])∧(+@z(cn[5], 1@z) →^* cn[1])∧(an[5] →^* an[1]))

(5) -> (2), if ((i[5] →^* i[2])∧(+@z(j[5], 1@z) →^* j[2])∧(bn[5] →^* bn[2])∧(+@z(cn[5], 1@z) →^* cn[2])∧(an[5] →^* an[2]))

(5) -> (6), if ((i[5] →^* i[6])∧(+@z(j[5], 1@z) →^* j[6])∧(bn[5] →^* bn[6])∧(+@z(cn[5], 1@z) →^* cn[6])∧(an[5] →^* an[6]))

(5) -> (7), if ((i[5] →^* i[7])∧(+@z(j[5], 1@z) →^* j[7])∧(bn[5] →^* bn[7])∧(+@z(cn[5], 1@z) →^* cn[7])∧(an[5] →^* an[7]))

(6) -> (0), if ((cn[6] →^* cn[0])∧(i[6] →^* i[0])∧(an[6] →^* an[0])∧(bn[6] →^* bn[0])∧(j[6] →^* j[0])∧(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])) →^* TRUE))

(7) -> (3), if ((cn[7] →^* cn[3])∧(i[7] →^* i[3])∧(an[7] →^* an[3])∧(bn[7] →^* bn[3])∧(j[7] →^* j[3])∧(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])) →^* TRUE))

eval(x0, x1, x2, x3, x4)
Cond_eval(TRUE, x0, x1, x2, x3, x4)
Cond_eval2(TRUE, x0, x1, x2, x3, x4)
Cond_eval3(TRUE, x0, x1, x2, x3, x4)
Cond_eval1(TRUE, x0, x1, x2, x3, x4)

• We consider the chain EVAL(an[6], bn[6], cn[6], i[6], j[6]) → COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6]), COND_EVAL(TRUE, an[0], bn[0], cn[0], i[0], j[0]) → EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0]) which results in the following constraint:
  

  (1)    (&&(<@z(j[6], bn[6]), <@z(i[6], an[6]))=TRUE∧j[6]=j[0]∧cn[6]=cn[0]∧an[6]=an[0]∧bn[6]=bn[0]∧i[6]=i[0] ⇒ COND_EVAL(TRUE, an[0], bn[0], cn[0], i[0], j[0])≥NonInfC∧COND_EVAL(TRUE, an[0], bn[0], cn[0], i[0], j[0])≥EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥))

  
  
  We simplified constraint (1) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:
  

  (2)    (<@z(j[6], bn[6])=TRUE∧<@z(i[6], an[6])=TRUE ⇒ COND_EVAL(TRUE, an[6], bn[6], cn[6], i[6], j[6])≥NonInfC∧COND_EVAL(TRUE, an[6], bn[6], cn[6], i[6], j[6])≥EVAL(an[6], bn[6], +@z(cn[6], 1@z), +@z(i[6], 1@z), j[6])∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥))

  
  
  We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (3)    (bn[6] + -1 + (-1)j[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ (U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (4)    (bn[6] + -1 + (-1)j[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ (U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (5)    (bn[6] + -1 + (-1)j[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ (U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧1 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (6)    (bn[6] + -1 + (-1)j[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  
  We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (7)    (bn[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  
  We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (8)    (bn[6] ≥ 0∧i[6] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  
  We simplified constraint (8) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (9)    (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  

  (10)    (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  
  We simplified constraint (9) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (11)    (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  

  (12)    (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  
  We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (13)    (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  

  (14)    (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  
  

• We consider the chain EVAL(an[1], bn[1], cn[1], i[1], j[1]) → COND_EVAL2(&&(<@z(j[1], bn[1]), <@z(i[1], an[1])), an[1], bn[1], cn[1], i[1], j[1]) which results in the following constraint:
  

  (15)    (EVAL(an[1], bn[1], cn[1], i[1], j[1])≥NonInfC∧EVAL(an[1], bn[1], cn[1], i[1], j[1])≥COND_EVAL2(&&(<@z(j[1], bn[1]), <@z(i[1], an[1])), an[1], bn[1], cn[1], i[1], j[1])∧(U^Increasing(COND_EVAL2(&&(<@z(j[1], bn[1]), <@z(i[1], an[1])), an[1], bn[1], cn[1], i[1], j[1])), ≥))

  
  
  We simplified constraint (15) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (16)    ((U^Increasing(COND_EVAL2(&&(<@z(j[1], bn[1]), <@z(i[1], an[1])), an[1], bn[1], cn[1], i[1], j[1])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (16) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (17)    ((U^Increasing(COND_EVAL2(&&(<@z(j[1], bn[1]), <@z(i[1], an[1])), an[1], bn[1], cn[1], i[1], j[1])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (17) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (18)    (0 ≥ 0∧(U^Increasing(COND_EVAL2(&&(<@z(j[1], bn[1]), <@z(i[1], an[1])), an[1], bn[1], cn[1], i[1], j[1])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (18) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (19)    (0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL2(&&(<@z(j[1], bn[1]), <@z(i[1], an[1])), an[1], bn[1], cn[1], i[1], j[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0)

  
  
  

• We consider the chain EVAL(an[2], bn[2], cn[2], i[2], j[2]) → COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2]) which results in the following constraint:
  

  (20)    (EVAL(an[2], bn[2], cn[2], i[2], j[2])≥NonInfC∧EVAL(an[2], bn[2], cn[2], i[2], j[2])≥COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])∧(U^Increasing(COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])), ≥))

  
  
  We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (21)    ((U^Increasing(COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (22)    ((U^Increasing(COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (23)    (1 ≥ 0∧(U^Increasing(COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (24)    (0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])), ≥)∧0 = 0∧1 ≥ 0∧0 = 0∧0 = 0)

  
  
  

• We consider the chain EVAL(an[7], bn[7], cn[7], i[7], j[7]) → COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7]), COND_EVAL3(TRUE, an[3], bn[3], cn[3], i[3], j[3]) → EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z)) which results in the following constraint:
  

  (25)    (i[7]=i[3]∧bn[7]=bn[3]∧cn[7]=cn[3]∧an[7]=an[3]∧j[7]=j[3]∧&&(<@z(j[7], bn[7]), >=@z(i[7], an[7]))=TRUE ⇒ COND_EVAL3(TRUE, an[3], bn[3], cn[3], i[3], j[3])≥NonInfC∧COND_EVAL3(TRUE, an[3], bn[3], cn[3], i[3], j[3])≥EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥))

  
  
  We simplified constraint (25) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:
  

  (26)    (<@z(j[7], bn[7])=TRUE∧>=@z(i[7], an[7])=TRUE ⇒ COND_EVAL3(TRUE, an[7], bn[7], cn[7], i[7], j[7])≥NonInfC∧COND_EVAL3(TRUE, an[7], bn[7], cn[7], i[7], j[7])≥EVAL(an[7], bn[7], +@z(cn[7], 1@z), i[7], +@z(j[7], 1@z))∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥))

  
  
  We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (27)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (28)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (29)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧1 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (30)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧1 ≥ 0∧0 = 0)

  
  
  We simplified constraint (30) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (31)    (-1 + bn[7] + (-1)j[7] ≥ 0∧an[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧1 ≥ 0∧0 = 0)

  
  
  We simplified constraint (31) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (32)    (j[7] ≥ 0∧an[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧1 ≥ 0∧0 = 0)

  
  
  We simplified constraint (32) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (33)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧1 ≥ 0∧0 = 0)

  
  

  (34)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧1 ≥ 0∧0 = 0)

  
  
  We simplified constraint (33) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (35)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧1 ≥ 0∧0 = 0)

  
  

  (36)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧1 ≥ 0∧0 = 0)

  
  
  We simplified constraint (34) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (37)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧1 ≥ 0∧0 = 0)

  
  

  (38)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧1 ≥ 0∧0 = 0)

  
  
  

• We consider the chain EVAL(an[2], bn[2], cn[2], i[2], j[2]) → COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2]), COND_EVAL1(TRUE, an[4], bn[4], cn[4], i[4], j[4]) → EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4]) which results in the following constraint:
  

  (39)    (&&(>=@z(j[2], bn[2]), <@z(i[2], an[2]))=TRUE∧an[2]=an[4]∧i[2]=i[4]∧bn[2]=bn[4]∧cn[2]=cn[4]∧j[2]=j[4] ⇒ COND_EVAL1(TRUE, an[4], bn[4], cn[4], i[4], j[4])≥NonInfC∧COND_EVAL1(TRUE, an[4], bn[4], cn[4], i[4], j[4])≥EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (39) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:
  

  (40)    (>=@z(j[2], bn[2])=TRUE∧<@z(i[2], an[2])=TRUE ⇒ COND_EVAL1(TRUE, an[2], bn[2], cn[2], i[2], j[2])≥NonInfC∧COND_EVAL1(TRUE, an[2], bn[2], cn[2], i[2], j[2])≥EVAL(an[2], bn[2], +@z(cn[2], 1@z), +@z(i[2], 1@z), j[2])∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (40) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (41)    (j[2] + (-1)bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ (U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (41) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (42)    (j[2] + (-1)bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ (U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (42) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (43)    (-1 + an[2] + (-1)i[2] ≥ 0∧j[2] + (-1)bn[2] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (43) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (44)    (-1 + an[2] + (-1)i[2] ≥ 0∧j[2] + (-1)bn[2] ≥ 0 ⇒ 0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (44) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (45)    (-1 + an[2] + (-1)i[2] ≥ 0∧bn[2] ≥ 0 ⇒ 0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (45) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (46)    (an[2] ≥ 0∧bn[2] ≥ 0 ⇒ 0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (46) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (47)    (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0 ⇒ 0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  

  (48)    (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0 ⇒ 0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (47) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (49)    (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  

  (50)    (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (48) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (51)    (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  

  (52)    (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  

• We consider the chain EVAL(an[1], bn[1], cn[1], i[1], j[1]) → COND_EVAL2(&&(<@z(j[1], bn[1]), <@z(i[1], an[1])), an[1], bn[1], cn[1], i[1], j[1]), COND_EVAL2(TRUE, an[5], bn[5], cn[5], i[5], j[5]) → EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z)) which results in the following constraint:
  

  (53)    (i[1]=i[5]∧cn[1]=cn[5]∧an[1]=an[5]∧bn[1]=bn[5]∧j[1]=j[5]∧&&(<@z(j[1], bn[1]), <@z(i[1], an[1]))=TRUE ⇒ COND_EVAL2(TRUE, an[5], bn[5], cn[5], i[5], j[5])≥NonInfC∧COND_EVAL2(TRUE, an[5], bn[5], cn[5], i[5], j[5])≥EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥))

  
  
  We simplified constraint (53) using rules (III), (IDP_BOOLEAN) which results in the following new constraint:
  

  (54)    (<@z(j[1], bn[1])=TRUE∧<@z(i[1], an[1])=TRUE ⇒ COND_EVAL2(TRUE, an[1], bn[1], cn[1], i[1], j[1])≥NonInfC∧COND_EVAL2(TRUE, an[1], bn[1], cn[1], i[1], j[1])≥EVAL(an[1], bn[1], +@z(cn[1], 1@z), i[1], +@z(j[1], 1@z))∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥))

  
  
  We simplified constraint (54) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (55)    (-1 + bn[1] + (-1)j[1] ≥ 0∧an[1] + -1 + (-1)i[1] ≥ 0 ⇒ (U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧-1 + (-1)Bound + (-1)j[1] + (-1)i[1] + bn[1] + an[1] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (55) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (56)    (-1 + bn[1] + (-1)j[1] ≥ 0∧an[1] + -1 + (-1)i[1] ≥ 0 ⇒ (U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧-1 + (-1)Bound + (-1)j[1] + (-1)i[1] + bn[1] + an[1] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (56) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (57)    (-1 + bn[1] + (-1)j[1] ≥ 0∧an[1] + -1 + (-1)i[1] ≥ 0 ⇒ (U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧-1 + (-1)Bound + (-1)j[1] + (-1)i[1] + bn[1] + an[1] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (57) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (58)    (-1 + bn[1] + (-1)j[1] ≥ 0∧an[1] + -1 + (-1)i[1] ≥ 0 ⇒ 0 ≥ 0∧-1 + (-1)Bound + (-1)j[1] + (-1)i[1] + bn[1] + an[1] ≥ 0∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧0 = 0∧0 = 0)

  
  
  We simplified constraint (58) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (59)    (j[1] ≥ 0∧an[1] + -1 + (-1)i[1] ≥ 0 ⇒ 0 ≥ 0∧(-1)Bound + j[1] + (-1)i[1] + an[1] ≥ 0∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧0 = 0∧0 = 0)

  
  
  We simplified constraint (59) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (60)    (j[1] ≥ 0∧an[1] ≥ 0 ⇒ 0 ≥ 0∧1 + (-1)Bound + j[1] + an[1] ≥ 0∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧0 = 0∧0 = 0)

  
  
  We simplified constraint (60) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (61)    (j[1] ≥ 0∧an[1] ≥ 0∧bn[1] ≥ 0 ⇒ 0 ≥ 0∧1 + (-1)Bound + j[1] + an[1] ≥ 0∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧0 = 0∧0 = 0)

  
  

  (62)    (j[1] ≥ 0∧an[1] ≥ 0∧bn[1] ≥ 0 ⇒ 0 ≥ 0∧1 + (-1)Bound + j[1] + an[1] ≥ 0∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧0 = 0∧0 = 0)

  
  
  We simplified constraint (61) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (63)    (j[1] ≥ 0∧an[1] ≥ 0∧bn[1] ≥ 0∧i[1] ≥ 0 ⇒ 0 ≥ 0∧1 + (-1)Bound + j[1] + an[1] ≥ 0∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧0 = 0∧0 = 0)

  
  

  (64)    (j[1] ≥ 0∧an[1] ≥ 0∧bn[1] ≥ 0∧i[1] ≥ 0 ⇒ 0 ≥ 0∧1 + (-1)Bound + j[1] + an[1] ≥ 0∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧0 = 0∧0 = 0)

  
  
  We simplified constraint (62) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (65)    (j[1] ≥ 0∧an[1] ≥ 0∧bn[1] ≥ 0∧i[1] ≥ 0 ⇒ 0 ≥ 0∧1 + (-1)Bound + j[1] + an[1] ≥ 0∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧0 = 0∧0 = 0)

  
  

  (66)    (j[1] ≥ 0∧an[1] ≥ 0∧bn[1] ≥ 0∧i[1] ≥ 0 ⇒ 0 ≥ 0∧1 + (-1)Bound + j[1] + an[1] ≥ 0∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧0 = 0∧0 = 0)

  
  
  

• We consider the chain EVAL(an[6], bn[6], cn[6], i[6], j[6]) → COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6]) which results in the following constraint:
  

  (67)    (EVAL(an[6], bn[6], cn[6], i[6], j[6])≥NonInfC∧EVAL(an[6], bn[6], cn[6], i[6], j[6])≥COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6])∧(U^Increasing(COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6])), ≥))

  
  
  We simplified constraint (67) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (68)    ((U^Increasing(COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (68) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (69)    ((U^Increasing(COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (69) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (70)    ((U^Increasing(COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (70) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (71)    (0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0)

  
  
  

• We consider the chain EVAL(an[7], bn[7], cn[7], i[7], j[7]) → COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7]) which results in the following constraint:
  

  (72)    (EVAL(an[7], bn[7], cn[7], i[7], j[7])≥NonInfC∧EVAL(an[7], bn[7], cn[7], i[7], j[7])≥COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])∧(U^Increasing(COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])), ≥))

  
  
  We simplified constraint (72) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (73)    ((U^Increasing(COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (73) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (74)    ((U^Increasing(COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (74) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (75)    (0 ≥ 0∧(U^Increasing(COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (75) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (76)    ((U^Increasing(COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0)

  
  
  

• COND_EVAL(TRUE, an, bn, cn, i, j) → EVAL(an, bn, +@z(cn, 1@z), +@z(i, 1@z), j)
  
  • (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)
    
  • (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)
    
  • (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)
    
  • (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 1 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)
    
  
  
• EVAL(an, bn, cn, i, j) → COND_EVAL2(&&(<@z(j, bn), <@z(i, an)), an, bn, cn, i, j)
  
  • (0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL2(&&(<@z(j[1], bn[1]), <@z(i[1], an[1])), an[1], bn[1], cn[1], i[1], j[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧0 = 0∧0 = 0)
    
  
  
• EVAL(an, bn, cn, i, j) → COND_EVAL1(&&(>=@z(j, bn), <@z(i, an)), an, bn, cn, i, j)
  
  • (0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])), ≥)∧0 = 0∧1 ≥ 0∧0 = 0∧0 = 0)
    
  
  
• COND_EVAL3(TRUE, an, bn, cn, i, j) → EVAL(an, bn, +@z(cn, 1@z), i, +@z(j, 1@z))
  
  • (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧1 ≥ 0∧0 = 0)
    
  • (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧1 ≥ 0∧0 = 0)
    
  • (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧1 ≥ 0∧0 = 0)
    
  • (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧1 ≥ 0∧0 = 0)
    
  
  
• COND_EVAL1(TRUE, an, bn, cn, i, j) → EVAL(an, bn, +@z(cn, 1@z), +@z(i, 1@z), j)
  
  • (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))
    
  • (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))
    
  • (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))
    
  • (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 = 0∧0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))
    
  
  
• COND_EVAL2(TRUE, an, bn, cn, i, j) → EVAL(an, bn, +@z(cn, 1@z), i, +@z(j, 1@z))
  
  • (j[1] ≥ 0∧an[1] ≥ 0∧bn[1] ≥ 0∧i[1] ≥ 0 ⇒ 0 ≥ 0∧1 + (-1)Bound + j[1] + an[1] ≥ 0∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧0 = 0∧0 = 0)
    
  • (j[1] ≥ 0∧an[1] ≥ 0∧bn[1] ≥ 0∧i[1] ≥ 0 ⇒ 0 ≥ 0∧1 + (-1)Bound + j[1] + an[1] ≥ 0∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧0 = 0∧0 = 0)
    
  • (j[1] ≥ 0∧an[1] ≥ 0∧bn[1] ≥ 0∧i[1] ≥ 0 ⇒ 0 ≥ 0∧1 + (-1)Bound + j[1] + an[1] ≥ 0∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧0 = 0∧0 = 0)
    
  • (j[1] ≥ 0∧an[1] ≥ 0∧bn[1] ≥ 0∧i[1] ≥ 0 ⇒ 0 ≥ 0∧1 + (-1)Bound + j[1] + an[1] ≥ 0∧(U^Increasing(EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))), ≥)∧0 = 0∧0 = 0)
    
  
  
• EVAL(an, bn, cn, i, j) → COND_EVAL(&&(<@z(j, bn), <@z(i, an)), an, bn, cn, i, j)
  
  • (0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0)
    
  
  
• EVAL(an, bn, cn, i, j) → COND_EVAL3(&&(<@z(j, bn), >=@z(i, an)), an, bn, cn, i, j)
  
  • ((U^Increasing(COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0)
    
  
  

POL(COND_EVAL2(x₁, x₂, x₃, x₄, x₅, x₆)) = -1 + (-1)x₆ + (-1)x₅ + x₃ + x₂   
POL(COND_EVAL3(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + (-1)x₆ + (-1)x₅ + x₃ + x₂ + (2)x₁   
POL(TRUE) = -1   
POL(&&(x₁, x₂)) = -1   
POL(FALSE) = -1   
POL(<@z(x₁, x₂)) = -1   
POL(EVAL(x₁, x₂, x₃, x₄, x₅)) = -1 + (-1)x₅ + (-1)x₄ + x₂ + x₁   
POL(COND_EVAL1(x₁, x₂, x₃, x₄, x₅, x₆)) = -1 + (-1)x₆ + (-1)x₅ + x₃ + x₂ + x₁   
POL(>=@z(x₁, x₂)) = -1   
POL(+@z(x₁, x₂)) = x₁ + x₂   
POL(COND_EVAL(x₁, x₂, x₃, x₄, x₅, x₆)) = -1 + (-1)x₆ + (-1)x₅ + x₃ + x₂   
POL(1@z) = 1   
POL(undefined) = -1   

COND_EVAL2(TRUE, an[5], bn[5], cn[5], i[5], j[5]) → EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))

COND_EVAL2(TRUE, an[5], bn[5], cn[5], i[5], j[5]) → EVAL(an[5], bn[5], +@z(cn[5], 1@z), i[5], +@z(j[5], 1@z))

COND_EVAL(TRUE, an[0], bn[0], cn[0], i[0], j[0]) → EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])
EVAL(an[1], bn[1], cn[1], i[1], j[1]) → COND_EVAL2(&&(<@z(j[1], bn[1]), <@z(i[1], an[1])), an[1], bn[1], cn[1], i[1], j[1])
EVAL(an[2], bn[2], cn[2], i[2], j[2]) → COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])
COND_EVAL3(TRUE, an[3], bn[3], cn[3], i[3], j[3]) → EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))
COND_EVAL1(TRUE, an[4], bn[4], cn[4], i[4], j[4]) → EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])
EVAL(an[6], bn[6], cn[6], i[6], j[6]) → COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6])
EVAL(an[7], bn[7], cn[7], i[7], j[7]) → COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])

&&(FALSE, FALSE)¹ ↔ FALSE¹
&&(TRUE, TRUE)¹ → TRUE¹
+@z¹ ↔
&&(TRUE, FALSE)¹ → FALSE¹
&&(FALSE, TRUE)¹ ↔ FALSE¹

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

            ↳ IDP

              ↳ IDependencyGraphProof

z

(0) -> (2), if ((+@z(i[0], 1@z) →^* i[2])∧(j[0] →^* j[2])∧(bn[0] →^* bn[2])∧(+@z(cn[0], 1@z) →^* cn[2])∧(an[0] →^* an[2]))

(4) -> (6), if ((+@z(i[4], 1@z) →^* i[6])∧(j[4] →^* j[6])∧(bn[4] →^* bn[6])∧(+@z(cn[4], 1@z) →^* cn[6])∧(an[4] →^* an[6]))

(6) -> (0), if ((cn[6] →^* cn[0])∧(i[6] →^* i[0])∧(an[6] →^* an[0])∧(bn[6] →^* bn[0])∧(j[6] →^* j[0])∧(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])) →^* TRUE))

(3) -> (7), if ((i[3] →^* i[7])∧(+@z(j[3], 1@z) →^* j[7])∧(bn[3] →^* bn[7])∧(+@z(cn[3], 1@z) →^* cn[7])∧(an[3] →^* an[7]))

(0) -> (6), if ((+@z(i[0], 1@z) →^* i[6])∧(j[0] →^* j[6])∧(bn[0] →^* bn[6])∧(+@z(cn[0], 1@z) →^* cn[6])∧(an[0] →^* an[6]))

(7) -> (3), if ((cn[7] →^* cn[3])∧(i[7] →^* i[3])∧(an[7] →^* an[3])∧(bn[7] →^* bn[3])∧(j[7] →^* j[3])∧(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])) →^* TRUE))

(0) -> (7), if ((+@z(i[0], 1@z) →^* i[7])∧(j[0] →^* j[7])∧(bn[0] →^* bn[7])∧(+@z(cn[0], 1@z) →^* cn[7])∧(an[0] →^* an[7]))

(4) -> (2), if ((+@z(i[4], 1@z) →^* i[2])∧(j[4] →^* j[2])∧(bn[4] →^* bn[2])∧(+@z(cn[4], 1@z) →^* cn[2])∧(an[4] →^* an[2]))

(2) -> (4), if ((cn[2] →^* cn[4])∧(i[2] →^* i[4])∧(an[2] →^* an[4])∧(bn[2] →^* bn[4])∧(j[2] →^* j[4])∧(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])) →^* TRUE))

(4) -> (7), if ((+@z(i[4], 1@z) →^* i[7])∧(j[4] →^* j[7])∧(bn[4] →^* bn[7])∧(+@z(cn[4], 1@z) →^* cn[7])∧(an[4] →^* an[7]))

(3) -> (2), if ((i[3] →^* i[2])∧(+@z(j[3], 1@z) →^* j[2])∧(bn[3] →^* bn[2])∧(+@z(cn[3], 1@z) →^* cn[2])∧(an[3] →^* an[2]))

(0) -> (1), if ((+@z(i[0], 1@z) →^* i[1])∧(j[0] →^* j[1])∧(bn[0] →^* bn[1])∧(+@z(cn[0], 1@z) →^* cn[1])∧(an[0] →^* an[1]))

(3) -> (6), if ((i[3] →^* i[6])∧(+@z(j[3], 1@z) →^* j[6])∧(bn[3] →^* bn[6])∧(+@z(cn[3], 1@z) →^* cn[6])∧(an[3] →^* an[6]))

(4) -> (1), if ((+@z(i[4], 1@z) →^* i[1])∧(j[4] →^* j[1])∧(bn[4] →^* bn[1])∧(+@z(cn[4], 1@z) →^* cn[1])∧(an[4] →^* an[1]))

(3) -> (1), if ((i[3] →^* i[1])∧(+@z(j[3], 1@z) →^* j[1])∧(bn[3] →^* bn[1])∧(+@z(cn[3], 1@z) →^* cn[1])∧(an[3] →^* an[1]))

eval(x0, x1, x2, x3, x4)
Cond_eval(TRUE, x0, x1, x2, x3, x4)
Cond_eval2(TRUE, x0, x1, x2, x3, x4)
Cond_eval3(TRUE, x0, x1, x2, x3, x4)
Cond_eval1(TRUE, x0, x1, x2, x3, x4)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDPNonInfProof

            ↳ IDP

              ↳ IDependencyGraphProof

                ↳ IDP

                  ↳ IDPNonInfProof

z

(4) -> (2), if ((+@z(i[4], 1@z) →^* i[2])∧(j[4] →^* j[2])∧(bn[4] →^* bn[2])∧(+@z(cn[4], 1@z) →^* cn[2])∧(an[4] →^* an[2]))

(0) -> (2), if ((+@z(i[0], 1@z) →^* i[2])∧(j[0] →^* j[2])∧(bn[0] →^* bn[2])∧(+@z(cn[0], 1@z) →^* cn[2])∧(an[0] →^* an[2]))

(4) -> (6), if ((+@z(i[4], 1@z) →^* i[6])∧(j[4] →^* j[6])∧(bn[4] →^* bn[6])∧(+@z(cn[4], 1@z) →^* cn[6])∧(an[4] →^* an[6]))

(2) -> (4), if ((cn[2] →^* cn[4])∧(i[2] →^* i[4])∧(an[2] →^* an[4])∧(bn[2] →^* bn[4])∧(j[2] →^* j[4])∧(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])) →^* TRUE))

(6) -> (0), if ((cn[6] →^* cn[0])∧(i[6] →^* i[0])∧(an[6] →^* an[0])∧(bn[6] →^* bn[0])∧(j[6] →^* j[0])∧(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])) →^* TRUE))

(3) -> (2), if ((i[3] →^* i[2])∧(+@z(j[3], 1@z) →^* j[2])∧(bn[3] →^* bn[2])∧(+@z(cn[3], 1@z) →^* cn[2])∧(an[3] →^* an[2]))

(4) -> (7), if ((+@z(i[4], 1@z) →^* i[7])∧(j[4] →^* j[7])∧(bn[4] →^* bn[7])∧(+@z(cn[4], 1@z) →^* cn[7])∧(an[4] →^* an[7]))

(3) -> (7), if ((i[3] →^* i[7])∧(+@z(j[3], 1@z) →^* j[7])∧(bn[3] →^* bn[7])∧(+@z(cn[3], 1@z) →^* cn[7])∧(an[3] →^* an[7]))

(3) -> (6), if ((i[3] →^* i[6])∧(+@z(j[3], 1@z) →^* j[6])∧(bn[3] →^* bn[6])∧(+@z(cn[3], 1@z) →^* cn[6])∧(an[3] →^* an[6]))

(0) -> (6), if ((+@z(i[0], 1@z) →^* i[6])∧(j[0] →^* j[6])∧(bn[0] →^* bn[6])∧(+@z(cn[0], 1@z) →^* cn[6])∧(an[0] →^* an[6]))

(7) -> (3), if ((cn[7] →^* cn[3])∧(i[7] →^* i[3])∧(an[7] →^* an[3])∧(bn[7] →^* bn[3])∧(j[7] →^* j[3])∧(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])) →^* TRUE))

(0) -> (7), if ((+@z(i[0], 1@z) →^* i[7])∧(j[0] →^* j[7])∧(bn[0] →^* bn[7])∧(+@z(cn[0], 1@z) →^* cn[7])∧(an[0] →^* an[7]))

eval(x0, x1, x2, x3, x4)
Cond_eval(TRUE, x0, x1, x2, x3, x4)
Cond_eval2(TRUE, x0, x1, x2, x3, x4)
Cond_eval3(TRUE, x0, x1, x2, x3, x4)
Cond_eval1(TRUE, x0, x1, x2, x3, x4)

• We consider the chain EVAL(an[2], bn[2], cn[2], i[2], j[2]) → COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2]), COND_EVAL1(TRUE, an[4], bn[4], cn[4], i[4], j[4]) → EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4]), EVAL(an[7], bn[7], cn[7], i[7], j[7]) → COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7]) which results in the following constraint:
  

  (1)    (+@z(cn[4], 1@z)=cn[7]∧an[4]=an[7]∧&&(>=@z(j[2], bn[2]), <@z(i[2], an[2]))=TRUE∧an[2]=an[4]∧i[2]=i[4]∧bn[2]=bn[4]∧+@z(i[4], 1@z)=i[7]∧bn[4]=bn[7]∧cn[2]=cn[4]∧j[2]=j[4]∧j[4]=j[7] ⇒ COND_EVAL1(TRUE, an[4], bn[4], cn[4], i[4], j[4])≥NonInfC∧COND_EVAL1(TRUE, an[4], bn[4], cn[4], i[4], j[4])≥EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (1) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (2)    (>=@z(j[2], bn[2])=TRUE∧<@z(i[2], an[2])=TRUE ⇒ COND_EVAL1(TRUE, an[2], bn[2], cn[2], i[2], j[2])≥NonInfC∧COND_EVAL1(TRUE, an[2], bn[2], cn[2], i[2], j[2])≥EVAL(an[2], bn[2], +@z(cn[2], 1@z), +@z(i[2], 1@z), j[2])∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (3)    (j[2] + (-1)bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ (U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (4)    (j[2] + (-1)bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ (U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (5)    (j[2] + (-1)bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (6)    (j[2] + (-1)bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  
  We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (7)    (bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  
  We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (8)    (bn[2] ≥ 0∧an[2] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  
  We simplified constraint (8) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (9)    (bn[2] ≥ 0∧an[2] ≥ 0∧i[2] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  

  (10)    (bn[2] ≥ 0∧an[2] ≥ 0∧i[2] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  
  We simplified constraint (9) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (11)    (bn[2] ≥ 0∧an[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  

  (12)    (bn[2] ≥ 0∧an[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  
  We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (13)    (bn[2] ≥ 0∧an[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  

  (14)    (bn[2] ≥ 0∧an[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 ≥ 0∧0 = 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  
  
• We consider the chain EVAL(an[2], bn[2], cn[2], i[2], j[2]) → COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2]), COND_EVAL1(TRUE, an[4], bn[4], cn[4], i[4], j[4]) → EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4]), EVAL(an[6], bn[6], cn[6], i[6], j[6]) → COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6]) which results in the following constraint:
  

  (15)    (an[4]=an[6]∧j[4]=j[6]∧&&(>=@z(j[2], bn[2]), <@z(i[2], an[2]))=TRUE∧an[2]=an[4]∧i[2]=i[4]∧+@z(cn[4], 1@z)=cn[6]∧bn[2]=bn[4]∧cn[2]=cn[4]∧+@z(i[4], 1@z)=i[6]∧j[2]=j[4]∧bn[4]=bn[6] ⇒ COND_EVAL1(TRUE, an[4], bn[4], cn[4], i[4], j[4])≥NonInfC∧COND_EVAL1(TRUE, an[4], bn[4], cn[4], i[4], j[4])≥EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (15) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (16)    (>=@z(j[2], bn[2])=TRUE∧<@z(i[2], an[2])=TRUE ⇒ COND_EVAL1(TRUE, an[2], bn[2], cn[2], i[2], j[2])≥NonInfC∧COND_EVAL1(TRUE, an[2], bn[2], cn[2], i[2], j[2])≥EVAL(an[2], bn[2], +@z(cn[2], 1@z), +@z(i[2], 1@z), j[2])∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (16) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (17)    (j[2] + (-1)bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ (U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (17) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (18)    (j[2] + (-1)bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ (U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (18) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (19)    (j[2] + (-1)bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (19) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (20)    (j[2] + (-1)bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ 0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (20) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (21)    (bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ 0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (21) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (22)    (bn[2] ≥ 0∧an[2] ≥ 0 ⇒ 0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (22) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (23)    (bn[2] ≥ 0∧an[2] ≥ 0∧i[2] ≥ 0 ⇒ 0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  

  (24)    (bn[2] ≥ 0∧an[2] ≥ 0∧i[2] ≥ 0 ⇒ 0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (23) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (25)    (bn[2] ≥ 0∧an[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  

  (26)    (bn[2] ≥ 0∧an[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (24) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (27)    (bn[2] ≥ 0∧an[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  

  (28)    (bn[2] ≥ 0∧an[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  
• We consider the chain EVAL(an[2], bn[2], cn[2], i[2], j[2]) → COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2]), COND_EVAL1(TRUE, an[4], bn[4], cn[4], i[4], j[4]) → EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4]), EVAL(an[2], bn[2], cn[2], i[2], j[2]) → COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2]) which results in the following constraint:
  

  (29)    (an[4]=an[2]1∧+@z(cn[4], 1@z)=cn[2]1∧&&(>=@z(j[2], bn[2]), <@z(i[2], an[2]))=TRUE∧an[2]=an[4]∧i[2]=i[4]∧bn[4]=bn[2]1∧bn[2]=bn[4]∧cn[2]=cn[4]∧+@z(i[4], 1@z)=i[2]1∧j[2]=j[4]∧j[4]=j[2]1 ⇒ COND_EVAL1(TRUE, an[4], bn[4], cn[4], i[4], j[4])≥NonInfC∧COND_EVAL1(TRUE, an[4], bn[4], cn[4], i[4], j[4])≥EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (29) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (30)    (>=@z(j[2], bn[2])=TRUE∧<@z(i[2], an[2])=TRUE ⇒ COND_EVAL1(TRUE, an[2], bn[2], cn[2], i[2], j[2])≥NonInfC∧COND_EVAL1(TRUE, an[2], bn[2], cn[2], i[2], j[2])≥EVAL(an[2], bn[2], +@z(cn[2], 1@z), +@z(i[2], 1@z), j[2])∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (30) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (31)    (j[2] + (-1)bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ (U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (31) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (32)    (j[2] + (-1)bn[2] ≥ 0∧-1 + an[2] + (-1)i[2] ≥ 0 ⇒ (U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (32) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (33)    (-1 + an[2] + (-1)i[2] ≥ 0∧j[2] + (-1)bn[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥))

  
  
  We simplified constraint (33) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (34)    (-1 + an[2] + (-1)i[2] ≥ 0∧j[2] + (-1)bn[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  
  We simplified constraint (34) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (35)    (-1 + an[2] + (-1)i[2] ≥ 0∧bn[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  
  We simplified constraint (35) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (36)    (an[2] ≥ 0∧bn[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  
  We simplified constraint (36) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (37)    (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  

  (38)    (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  
  We simplified constraint (37) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (39)    (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  

  (40)    (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  
  We simplified constraint (38) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (41)    (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  

  (42)    (an[2] ≥ 0∧bn[2] ≥ 0∧i[2] ≥ 0∧j[2] ≥ 0 ⇒ 0 ≥ 0∧0 ≥ 0∧0 = 0∧(U^Increasing(EVAL(an[4], bn[4], +@z(cn[4], 1@z), +@z(i[4], 1@z), j[4])), ≥)∧0 = 0)

  
  
  

• We consider the chain EVAL(an[2], bn[2], cn[2], i[2], j[2]) → COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2]) which results in the following constraint:
  

  (43)    (EVAL(an[2], bn[2], cn[2], i[2], j[2])≥NonInfC∧EVAL(an[2], bn[2], cn[2], i[2], j[2])≥COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])∧(U^Increasing(COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])), ≥))

  
  
  We simplified constraint (43) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (44)    ((U^Increasing(COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (44) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (45)    ((U^Increasing(COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (45) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (46)    (0 ≥ 0∧(U^Increasing(COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (46) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (47)    (0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 ≥ 0∧0 = 0∧0 = 0∧(U^Increasing(COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0)

  
  
  

• We consider the chain EVAL(an[7], bn[7], cn[7], i[7], j[7]) → COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7]), COND_EVAL3(TRUE, an[3], bn[3], cn[3], i[3], j[3]) → EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z)), EVAL(an[2], bn[2], cn[2], i[2], j[2]) → COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2]) which results in the following constraint:
  

  (48)    (i[7]=i[3]∧bn[7]=bn[3]∧cn[7]=cn[3]∧i[3]=i[2]∧bn[3]=bn[2]∧an[3]=an[2]∧an[7]=an[3]∧+@z(j[3], 1@z)=j[2]∧j[7]=j[3]∧+@z(cn[3], 1@z)=cn[2]∧&&(<@z(j[7], bn[7]), >=@z(i[7], an[7]))=TRUE ⇒ COND_EVAL3(TRUE, an[3], bn[3], cn[3], i[3], j[3])≥NonInfC∧COND_EVAL3(TRUE, an[3], bn[3], cn[3], i[3], j[3])≥EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥))

  
  
  We simplified constraint (48) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (49)    (<@z(j[7], bn[7])=TRUE∧>=@z(i[7], an[7])=TRUE ⇒ COND_EVAL3(TRUE, an[7], bn[7], cn[7], i[7], j[7])≥NonInfC∧COND_EVAL3(TRUE, an[7], bn[7], cn[7], i[7], j[7])≥EVAL(an[7], bn[7], +@z(cn[7], 1@z), i[7], +@z(j[7], 1@z))∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥))

  
  
  We simplified constraint (49) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (50)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (50) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (51)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (51) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (52)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (52) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (53)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  
  We simplified constraint (53) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (54)    (-1 + bn[7] + (-1)j[7] ≥ 0∧an[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  
  We simplified constraint (54) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (55)    (j[7] ≥ 0∧an[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  
  We simplified constraint (55) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (56)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  

  (57)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  
  We simplified constraint (56) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (58)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  

  (59)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  
  We simplified constraint (57) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (60)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  

  (61)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 = 0∧0 = 0)

  
  
  
• We consider the chain EVAL(an[7], bn[7], cn[7], i[7], j[7]) → COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7]), COND_EVAL3(TRUE, an[3], bn[3], cn[3], i[3], j[3]) → EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z)), EVAL(an[7], bn[7], cn[7], i[7], j[7]) → COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7]) which results in the following constraint:
  

  (62)    (an[3]=an[7]1∧i[7]=i[3]∧bn[3]=bn[7]1∧+@z(cn[3], 1@z)=cn[7]1∧bn[7]=bn[3]∧cn[7]=cn[3]∧+@z(j[3], 1@z)=j[7]1∧i[3]=i[7]1∧an[7]=an[3]∧j[7]=j[3]∧&&(<@z(j[7], bn[7]), >=@z(i[7], an[7]))=TRUE ⇒ COND_EVAL3(TRUE, an[3], bn[3], cn[3], i[3], j[3])≥NonInfC∧COND_EVAL3(TRUE, an[3], bn[3], cn[3], i[3], j[3])≥EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥))

  
  
  We simplified constraint (62) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (63)    (<@z(j[7], bn[7])=TRUE∧>=@z(i[7], an[7])=TRUE ⇒ COND_EVAL3(TRUE, an[7], bn[7], cn[7], i[7], j[7])≥NonInfC∧COND_EVAL3(TRUE, an[7], bn[7], cn[7], i[7], j[7])≥EVAL(an[7], bn[7], +@z(cn[7], 1@z), i[7], +@z(j[7], 1@z))∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥))

  
  
  We simplified constraint (63) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (64)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (64) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (65)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (65) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (66)    (i[7] + (-1)an[7] ≥ 0∧-1 + bn[7] + (-1)j[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (66) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (67)    (i[7] + (-1)an[7] ≥ 0∧-1 + bn[7] + (-1)j[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (67) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (68)    (an[7] ≥ 0∧-1 + bn[7] + (-1)j[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (68) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (69)    (an[7] ≥ 0∧j[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (69) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (70)    (an[7] ≥ 0∧j[7] ≥ 0∧bn[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0)

  
  

  (71)    (an[7] ≥ 0∧j[7] ≥ 0∧bn[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (70) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (72)    (an[7] ≥ 0∧j[7] ≥ 0∧bn[7] ≥ 0∧i[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0)

  
  

  (73)    (an[7] ≥ 0∧j[7] ≥ 0∧bn[7] ≥ 0∧i[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (71) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (74)    (an[7] ≥ 0∧j[7] ≥ 0∧bn[7] ≥ 0∧i[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0)

  
  

  (75)    (an[7] ≥ 0∧j[7] ≥ 0∧bn[7] ≥ 0∧i[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0∧0 ≥ 0)

  
  
  
• We consider the chain EVAL(an[7], bn[7], cn[7], i[7], j[7]) → COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7]), COND_EVAL3(TRUE, an[3], bn[3], cn[3], i[3], j[3]) → EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z)), EVAL(an[6], bn[6], cn[6], i[6], j[6]) → COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6]) which results in the following constraint:
  

  (76)    (bn[3]=bn[6]∧i[7]=i[3]∧bn[7]=bn[3]∧cn[7]=cn[3]∧+@z(cn[3], 1@z)=cn[6]∧an[3]=an[6]∧i[3]=i[6]∧an[7]=an[3]∧j[7]=j[3]∧&&(<@z(j[7], bn[7]), >=@z(i[7], an[7]))=TRUE∧+@z(j[3], 1@z)=j[6] ⇒ COND_EVAL3(TRUE, an[3], bn[3], cn[3], i[3], j[3])≥NonInfC∧COND_EVAL3(TRUE, an[3], bn[3], cn[3], i[3], j[3])≥EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥))

  
  
  We simplified constraint (76) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (77)    (<@z(j[7], bn[7])=TRUE∧>=@z(i[7], an[7])=TRUE ⇒ COND_EVAL3(TRUE, an[7], bn[7], cn[7], i[7], j[7])≥NonInfC∧COND_EVAL3(TRUE, an[7], bn[7], cn[7], i[7], j[7])≥EVAL(an[7], bn[7], +@z(cn[7], 1@z), i[7], +@z(j[7], 1@z))∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥))

  
  
  We simplified constraint (77) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (78)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (78) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (79)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (79) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (80)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ (U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (80) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (81)    (-1 + bn[7] + (-1)j[7] ≥ 0∧i[7] + (-1)an[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0)

  
  
  We simplified constraint (81) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (82)    (-1 + bn[7] + (-1)j[7] ≥ 0∧an[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0)

  
  
  We simplified constraint (82) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (83)    (j[7] ≥ 0∧an[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0)

  
  
  We simplified constraint (83) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (84)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0)

  
  

  (85)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0)

  
  
  We simplified constraint (84) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (86)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0)

  
  

  (87)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0)

  
  
  We simplified constraint (85) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (88)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0)

  
  

  (89)    (j[7] ≥ 0∧an[7] ≥ 0∧i[7] ≥ 0∧bn[7] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[3], bn[3], +@z(cn[3], 1@z), i[3], +@z(j[3], 1@z))), ≥)∧0 = 0∧0 = 0∧0 ≥ 0)

  
  
  

• We consider the chain EVAL(an[7], bn[7], cn[7], i[7], j[7]) → COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7]) which results in the following constraint:
  

  (90)    (EVAL(an[7], bn[7], cn[7], i[7], j[7])≥NonInfC∧EVAL(an[7], bn[7], cn[7], i[7], j[7])≥COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])∧(U^Increasing(COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])), ≥))

  
  
  We simplified constraint (90) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (91)    ((U^Increasing(COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (91) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (92)    ((U^Increasing(COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])), ≥)∧0 ≥ 0∧1 ≥ 0)

  
  
  We simplified constraint (92) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (93)    (0 ≥ 0∧(U^Increasing(COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])), ≥)∧1 ≥ 0)

  
  
  We simplified constraint (93) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (94)    (0 = 0∧0 = 0∧0 ≥ 0∧(U^Increasing(COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧1 ≥ 0)

  
  
  

• We consider the chain EVAL(an[6], bn[6], cn[6], i[6], j[6]) → COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6]), COND_EVAL(TRUE, an[0], bn[0], cn[0], i[0], j[0]) → EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0]), EVAL(an[7], bn[7], cn[7], i[7], j[7]) → COND_EVAL3(&&(<@z(j[7], bn[7]), >=@z(i[7], an[7])), an[7], bn[7], cn[7], i[7], j[7]) which results in the following constraint:
  

  (95)    (+@z(cn[0], 1@z)=cn[7]∧&&(<@z(j[6], bn[6]), <@z(i[6], an[6]))=TRUE∧an[0]=an[7]∧j[6]=j[0]∧cn[6]=cn[0]∧+@z(i[0], 1@z)=i[7]∧an[6]=an[0]∧bn[6]=bn[0]∧i[6]=i[0]∧bn[0]=bn[7]∧j[0]=j[7] ⇒ COND_EVAL(TRUE, an[0], bn[0], cn[0], i[0], j[0])≥NonInfC∧COND_EVAL(TRUE, an[0], bn[0], cn[0], i[0], j[0])≥EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥))

  
  
  We simplified constraint (95) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (96)    (<@z(j[6], bn[6])=TRUE∧<@z(i[6], an[6])=TRUE ⇒ COND_EVAL(TRUE, an[6], bn[6], cn[6], i[6], j[6])≥NonInfC∧COND_EVAL(TRUE, an[6], bn[6], cn[6], i[6], j[6])≥EVAL(an[6], bn[6], +@z(cn[6], 1@z), +@z(i[6], 1@z), j[6])∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥))

  
  
  We simplified constraint (96) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (97)    (bn[6] + -1 + (-1)j[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ (U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧-1 + (-1)Bound + (-1)j[6] + (-1)i[6] + bn[6] + an[6] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (97) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (98)    (bn[6] + -1 + (-1)j[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ (U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧-1 + (-1)Bound + (-1)j[6] + (-1)i[6] + bn[6] + an[6] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (98) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (99)    (-1 + an[6] + (-1)i[6] ≥ 0∧bn[6] + -1 + (-1)j[6] ≥ 0 ⇒ (U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧-1 + (-1)Bound + (-1)j[6] + (-1)i[6] + bn[6] + an[6] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (99) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (100)    (-1 + an[6] + (-1)i[6] ≥ 0∧bn[6] + -1 + (-1)j[6] ≥ 0 ⇒ 0 = 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧-1 + (-1)Bound + (-1)j[6] + (-1)i[6] + bn[6] + an[6] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (100) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (101)    (-1 + an[6] + (-1)i[6] ≥ 0∧bn[6] ≥ 0 ⇒ 0 = 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧(-1)Bound + (-1)i[6] + bn[6] + an[6] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (101) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (102)    (i[6] ≥ 0∧bn[6] ≥ 0 ⇒ 0 = 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (102) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (103)    (i[6] ≥ 0∧bn[6] ≥ 0∧j[6] ≥ 0 ⇒ 0 = 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0∧0 ≥ 0)

  
  

  (104)    (i[6] ≥ 0∧bn[6] ≥ 0∧j[6] ≥ 0 ⇒ 0 = 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (103) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (105)    (i[6] ≥ 0∧bn[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 0 = 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0∧0 ≥ 0)

  
  

  (106)    (i[6] ≥ 0∧bn[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 0 = 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (104) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (107)    (i[6] ≥ 0∧bn[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 0 = 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0∧0 ≥ 0)

  
  

  (108)    (i[6] ≥ 0∧bn[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 0 = 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0∧0 ≥ 0)

  
  
  
• We consider the chain EVAL(an[6], bn[6], cn[6], i[6], j[6]) → COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6]), COND_EVAL(TRUE, an[0], bn[0], cn[0], i[0], j[0]) → EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0]), EVAL(an[2], bn[2], cn[2], i[2], j[2]) → COND_EVAL1(&&(>=@z(j[2], bn[2]), <@z(i[2], an[2])), an[2], bn[2], cn[2], i[2], j[2]) which results in the following constraint:
  

  (109)    (&&(<@z(j[6], bn[6]), <@z(i[6], an[6]))=TRUE∧j[6]=j[0]∧cn[6]=cn[0]∧bn[0]=bn[2]∧j[0]=j[2]∧an[6]=an[0]∧bn[6]=bn[0]∧i[6]=i[0]∧+@z(i[0], 1@z)=i[2]∧an[0]=an[2]∧+@z(cn[0], 1@z)=cn[2] ⇒ COND_EVAL(TRUE, an[0], bn[0], cn[0], i[0], j[0])≥NonInfC∧COND_EVAL(TRUE, an[0], bn[0], cn[0], i[0], j[0])≥EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥))

  
  
  We simplified constraint (109) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (110)    (<@z(j[6], bn[6])=TRUE∧<@z(i[6], an[6])=TRUE ⇒ COND_EVAL(TRUE, an[6], bn[6], cn[6], i[6], j[6])≥NonInfC∧COND_EVAL(TRUE, an[6], bn[6], cn[6], i[6], j[6])≥EVAL(an[6], bn[6], +@z(cn[6], 1@z), +@z(i[6], 1@z), j[6])∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥))

  
  
  We simplified constraint (110) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (111)    (bn[6] + -1 + (-1)j[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ (U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧-1 + (-1)Bound + (-1)j[6] + (-1)i[6] + bn[6] + an[6] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (111) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (112)    (bn[6] + -1 + (-1)j[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ (U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧-1 + (-1)Bound + (-1)j[6] + (-1)i[6] + bn[6] + an[6] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (112) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (113)    (-1 + an[6] + (-1)i[6] ≥ 0∧bn[6] + -1 + (-1)j[6] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧-1 + (-1)Bound + (-1)j[6] + (-1)i[6] + bn[6] + an[6] ≥ 0)

  
  
  We simplified constraint (113) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (114)    (-1 + an[6] + (-1)i[6] ≥ 0∧bn[6] + -1 + (-1)j[6] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 = 0∧-1 + (-1)Bound + (-1)j[6] + (-1)i[6] + bn[6] + an[6] ≥ 0)

  
  
  We simplified constraint (114) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (115)    (-1 + an[6] + (-1)i[6] ≥ 0∧bn[6] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 = 0∧(-1)Bound + (-1)i[6] + bn[6] + an[6] ≥ 0)

  
  
  We simplified constraint (115) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (116)    (i[6] ≥ 0∧bn[6] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0)

  
  
  We simplified constraint (116) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (117)    (i[6] ≥ 0∧bn[6] ≥ 0∧j[6] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0)

  
  

  (118)    (i[6] ≥ 0∧bn[6] ≥ 0∧j[6] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0)

  
  
  We simplified constraint (117) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (119)    (i[6] ≥ 0∧bn[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0)

  
  

  (120)    (i[6] ≥ 0∧bn[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0)

  
  
  We simplified constraint (118) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (121)    (i[6] ≥ 0∧bn[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0)

  
  

  (122)    (i[6] ≥ 0∧bn[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 0 ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 = 0∧1 + (-1)Bound + i[6] + bn[6] ≥ 0)

  
  
  
• We consider the chain EVAL(an[6], bn[6], cn[6], i[6], j[6]) → COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6]), COND_EVAL(TRUE, an[0], bn[0], cn[0], i[0], j[0]) → EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0]), EVAL(an[6], bn[6], cn[6], i[6], j[6]) → COND_EVAL(&&(<@z(j[6], bn[6]), <@z(i[6], an[6])), an[6], bn[6], cn[6], i[6], j[6]) which results in the following constraint:
  

  (123)    (an[0]=an[6]1∧&&(<@z(j[6], bn[6]), <@z(i[6], an[6]))=TRUE∧+@z(i[0], 1@z)=i[6]1∧j[6]=j[0]∧bn[0]=bn[6]1∧cn[6]=cn[0]∧+@z(cn[0], 1@z)=cn[6]1∧an[6]=an[0]∧bn[6]=bn[0]∧i[6]=i[0]∧j[0]=j[6]1 ⇒ COND_EVAL(TRUE, an[0], bn[0], cn[0], i[0], j[0])≥NonInfC∧COND_EVAL(TRUE, an[0], bn[0], cn[0], i[0], j[0])≥EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥))

  
  
  We simplified constraint (123) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
  

  (124)    (<@z(j[6], bn[6])=TRUE∧<@z(i[6], an[6])=TRUE ⇒ COND_EVAL(TRUE, an[6], bn[6], cn[6], i[6], j[6])≥NonInfC∧COND_EVAL(TRUE, an[6], bn[6], cn[6], i[6], j[6])≥EVAL(an[6], bn[6], +@z(cn[6], 1@z), +@z(i[6], 1@z), j[6])∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥))

  
  
  We simplified constraint (124) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
  

  (125)    (bn[6] + -1 + (-1)j[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ (U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧-1 + (-1)Bound + (-1)j[6] + (-1)i[6] + bn[6] + an[6] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (125) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
  

  (126)    (bn[6] + -1 + (-1)j[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ (U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧-1 + (-1)Bound + (-1)j[6] + (-1)i[6] + bn[6] + an[6] ≥ 0∧0 ≥ 0)

  
  
  We simplified constraint (126) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
  

  (127)    (bn[6] + -1 + (-1)j[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ -1 + (-1)Bound + (-1)j[6] + (-1)i[6] + bn[6] + an[6] ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 ≥ 0)

  
  
  We simplified constraint (127) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
  

  (128)    (bn[6] + -1 + (-1)j[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ -1 + (-1)Bound + (-1)j[6] + (-1)i[6] + bn[6] + an[6] ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0)

  
  
  We simplified constraint (128) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (129)    (bn[6] ≥ 0∧-1 + an[6] + (-1)i[6] ≥ 0 ⇒ (-1)Bound + (-1)i[6] + bn[6] + an[6] ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0)

  
  
  We simplified constraint (129) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
  

  (130)    (bn[6] ≥ 0∧i[6] ≥ 0 ⇒ 1 + (-1)Bound + i[6] + bn[6] ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0)

  
  
  We simplified constraint (130) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (131)    (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0 ⇒ 1 + (-1)Bound + i[6] + bn[6] ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0)

  
  

  (132)    (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0 ⇒ 1 + (-1)Bound + i[6] + bn[6] ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0)

  
  
  We simplified constraint (131) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (133)    (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 1 + (-1)Bound + i[6] + bn[6] ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0)

  
  

  (134)    (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 1 + (-1)Bound + i[6] + bn[6] ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0)

  
  
  We simplified constraint (132) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
  

  (135)    (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 1 + (-1)Bound + i[6] + bn[6] ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0)

  
  

  (136)    (bn[6] ≥ 0∧i[6] ≥ 0∧j[6] ≥ 0∧an[6] ≥ 0 ⇒ 1 + (-1)Bound + i[6] + bn[6] ≥ 0∧(U^Increasing(EVAL(an[0], bn[0], +@z(cn[0], 1@z), +@z(i[0], 1@z), j[0])), ≥)∧0 = 0∧0 ≥ 0∧0 = 0)